\begin{tabbing}
combine{-}ecl{-}tuples2($A$; $B$; $f$; $g$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$spreadn(\=$A$;\+
\\[0ex]${\it Ta}$,${\it ksa}$,${\it ia}$,${\it ga}$,${\it ha}$,${\it aa}$,${\it ea}$.spreadn
\\[0ex](\=$B$;\+
\\[0ex]${\it Tb}$,${\it ksb}$,${\it ib}$,${\it gb}$,${\it hb}$,${\it ab}$,${\it eb}$.$<$:${\it Ta}$ $\times$ (:${\it Tb}$ $\times$ (?$\mathbb{B}$))
\\[0ex], append(${\it ksa}$; ${\it ksb}$)
\\[0ex], $<$${\it ia}$, ${\it ib}$, inr $\cdot$ $>$
\\[0ex], $\lambda$${\it k'}$,$s$,$v$,$x$. let \=${\it sa}$ = if deq{-}member(Kind{-}deq; ${\it k'}$; ${\it ksa}$)\+
\\[0ex]then ${\it ga}$(${\it k'}$,$s$,$v$,$x$.1)
\\[0ex]else $x$.1
\\[0ex]f\=i  in\+
\\[0ex]let \=${\it sb}$ = if deq{-}member(Kind{-}deq; ${\it k'}$; ${\it ksb}$)\+
\\[0ex]then ${\it gb}$(${\it k'}$,$s$,$v$,($x$.2).1)
\\[0ex]else ($x$.2).1
\\[0ex]f\=i  in\+
\\[0ex]$<$${\it sa}$
\-\\[0ex], ${\it sb}$
\\[0ex], combine{-}halt{-}info(\=${\it ea}$;\+
\\[0ex]${\it eb}$;
\\[0ex]($\lambda$$m$.${\it ha}$($m$,${\it sa}$));
\\[0ex]($\lambda$$m$.${\it hb}$($m$,${\it sb}$));
\\[0ex]($x$.2.2))$>$
\-\-\-\-\\[0ex], $\lambda$$n$,$x$. $f$(($x$.2.2),$\lambda$$m$.${\it ha}$($m$,$x$.1),$\lambda$$m$.${\it hb}$($m$,($x$.2).1),$n$)
\\[0ex], $\lambda$$n$,${\it k'}$,$s$,$v$,$x$. \=$g$\+
\\[0ex](${\it ha}$(0,$x$.1)
\\[0ex],${\it hb}$(0,($x$.2).1)
\\[0ex],reduce(($\lambda$$m$,$b$. bor((${\it ha}$($m$,$x$.1)); $b$)); ff; ${\it ea}$)
\\[0ex],reduce(($\lambda$$m$,$b$. bor((${\it hb}$($m$,($x$.2).1)); $b$)); ff; ${\it eb}$)
\\[0ex],\=if deq{-}member(Kind{-}deq; ${\it k'}$; ${\it ksa}$)\+
\\[0ex]then ${\it aa}$($n$,${\it k'}$,$s$,$v$,$x$.1)
\\[0ex]else ff
\\[0ex]fi 
\-\\[0ex],\=if deq{-}member(Kind{-}deq; ${\it k'}$; ${\it ksb}$)\+
\\[0ex]then ${\it ab}$($n$,${\it k'}$,$s$,$v$,($x$.2).1)
\\[0ex]else ff
\\[0ex]fi )
\-\-\\[0ex], merge(${\it ea}$; ${\it eb}$)$>$))
\-\-
\end{tabbing}